0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 9 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 1763 ms)
↳10 BOUNDS(1, n^3)
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gcd(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → if3(gt(x, 0), x, y)
if2(true, x, y) → gcd(minus(x, y), y)
if2(false, x, y) → x
if3(true, x, y) → gcd(x, minus(y, x))
if3(false, x, y) → y
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x), y) → if(gt(s(x), y), x, y) [1]
if(true, x, y) → s(minus(x, y)) [1]
if(false, x, y) → 0 [1]
gcd(x, y) → if1(ge(x, y), x, y) [1]
if1(true, x, y) → if2(gt(y, 0), x, y) [1]
if1(false, x, y) → if3(gt(x, 0), x, y) [1]
if2(true, x, y) → gcd(minus(x, y), y) [1]
if2(false, x, y) → x [1]
if3(true, x, y) → gcd(x, minus(y, x)) [1]
if3(false, x, y) → y [1]
gt(0, y) → false [1]
gt(s(x), 0) → true [1]
gt(s(x), s(y)) → gt(x, y) [1]
ge(x, 0) → true [1]
ge(0, s(x)) → false [1]
ge(s(x), s(y)) → ge(x, y) [1]
minus(s(x), y) → if(gt(s(x), y), x, y) [1]
if(true, x, y) → s(minus(x, y)) [1]
if(false, x, y) → 0 [1]
gcd(x, y) → if1(ge(x, y), x, y) [1]
if1(true, x, y) → if2(gt(y, 0), x, y) [1]
if1(false, x, y) → if3(gt(x, 0), x, y) [1]
if2(true, x, y) → gcd(minus(x, y), y) [1]
if2(false, x, y) → x [1]
if3(true, x, y) → gcd(x, minus(y, x)) [1]
if3(false, x, y) → y [1]
gt(0, y) → false [1]
gt(s(x), 0) → true [1]
gt(s(x), s(y)) → gt(x, y) [1]
ge(x, 0) → true [1]
ge(0, s(x)) → false [1]
ge(s(x), s(y)) → ge(x, y) [1]
| minus :: s:0 → s:0 → s:0 s :: s:0 → s:0 if :: true:false → s:0 → s:0 → s:0 gt :: s:0 → s:0 → true:false true :: true:false false :: true:false 0 :: s:0 gcd :: s:0 → s:0 → s:0 if1 :: true:false → s:0 → s:0 → s:0 ge :: s:0 → s:0 → true:false if2 :: true:false → s:0 → s:0 → s:0 if3 :: true:false → s:0 → s:0 → s:0 |
minus(v0, v1) → null_minus [0]
gt(v0, v1) → null_gt [0]
ge(v0, v1) → null_ge [0]
if(v0, v1, v2) → null_if [0]
if1(v0, v1, v2) → null_if1 [0]
if2(v0, v1, v2) → null_if2 [0]
if3(v0, v1, v2) → null_if3 [0]
null_minus, null_gt, null_ge, null_if, null_if1, null_if2, null_if3
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
true => 2
false => 1
0 => 0
null_minus => 0
null_gt => 0
null_ge => 0
null_if => 0
null_if1 => 0
null_if2 => 0
null_if3 => 0
gcd(z, z') -{ 1 }→ if1(ge(x, y), x, y) :|: x >= 0, y >= 0, z = x, z' = y
ge(z, z') -{ 1 }→ ge(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
ge(z, z') -{ 1 }→ 2 :|: x >= 0, z = x, z' = 0
ge(z, z') -{ 1 }→ 1 :|: z' = 1 + x, x >= 0, z = 0
ge(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
gt(z, z') -{ 1 }→ gt(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
gt(z, z') -{ 1 }→ 2 :|: x >= 0, z = 1 + x, z' = 0
gt(z, z') -{ 1 }→ 1 :|: y >= 0, z = 0, z' = y
gt(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
if(z, z', z'') -{ 1 }→ 0 :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
if(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
if(z, z', z'') -{ 1 }→ 1 + minus(x, y) :|: z = 2, z' = x, z'' = y, x >= 0, y >= 0
if1(z, z', z'') -{ 1 }→ if3(gt(x, 0), x, y) :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
if1(z, z', z'') -{ 1 }→ if2(gt(y, 0), x, y) :|: z = 2, z' = x, z'' = y, x >= 0, y >= 0
if1(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
if2(z, z', z'') -{ 1 }→ x :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
if2(z, z', z'') -{ 1 }→ gcd(minus(x, y), y) :|: z = 2, z' = x, z'' = y, x >= 0, y >= 0
if2(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
if3(z, z', z'') -{ 1 }→ y :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
if3(z, z', z'') -{ 1 }→ gcd(x, minus(y, x)) :|: z = 2, z' = x, z'' = y, x >= 0, y >= 0
if3(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
minus(z, z') -{ 1 }→ if(gt(1 + x, y), x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
minus(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
| eq(start(V, V1, V4),0,[minus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V4),0,[if(V, V1, V4, Out)],[V >= 0,V1 >= 0,V4 >= 0]). eq(start(V, V1, V4),0,[gcd(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V4),0,[if1(V, V1, V4, Out)],[V >= 0,V1 >= 0,V4 >= 0]). eq(start(V, V1, V4),0,[if2(V, V1, V4, Out)],[V >= 0,V1 >= 0,V4 >= 0]). eq(start(V, V1, V4),0,[if3(V, V1, V4, Out)],[V >= 0,V1 >= 0,V4 >= 0]). eq(start(V, V1, V4),0,[gt(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V4),0,[ge(V, V1, Out)],[V >= 0,V1 >= 0]). eq(minus(V, V1, Out),1,[gt(1 + V2, V3, Ret0),if(Ret0, V2, V3, Ret)],[Out = Ret,V2 >= 0,V3 >= 0,V = 1 + V2,V1 = V3]). eq(if(V, V1, V4, Out),1,[minus(V5, V6, Ret1)],[Out = 1 + Ret1,V = 2,V1 = V5,V4 = V6,V5 >= 0,V6 >= 0]). eq(if(V, V1, V4, Out),1,[],[Out = 0,V1 = V7,V4 = V8,V = 1,V7 >= 0,V8 >= 0]). eq(gcd(V, V1, Out),1,[ge(V9, V10, Ret01),if1(Ret01, V9, V10, Ret2)],[Out = Ret2,V9 >= 0,V10 >= 0,V = V9,V1 = V10]). eq(if1(V, V1, V4, Out),1,[gt(V11, 0, Ret02),if2(Ret02, V12, V11, Ret3)],[Out = Ret3,V = 2,V1 = V12,V4 = V11,V12 >= 0,V11 >= 0]). eq(if1(V, V1, V4, Out),1,[gt(V13, 0, Ret03),if3(Ret03, V13, V14, Ret4)],[Out = Ret4,V1 = V13,V4 = V14,V = 1,V13 >= 0,V14 >= 0]). eq(if2(V, V1, V4, Out),1,[minus(V15, V16, Ret04),gcd(Ret04, V16, Ret5)],[Out = Ret5,V = 2,V1 = V15,V4 = V16,V15 >= 0,V16 >= 0]). eq(if2(V, V1, V4, Out),1,[],[Out = V17,V1 = V17,V4 = V18,V = 1,V17 >= 0,V18 >= 0]). eq(if3(V, V1, V4, Out),1,[minus(V20, V19, Ret11),gcd(V19, Ret11, Ret6)],[Out = Ret6,V = 2,V1 = V19,V4 = V20,V19 >= 0,V20 >= 0]). eq(if3(V, V1, V4, Out),1,[],[Out = V21,V1 = V22,V4 = V21,V = 1,V22 >= 0,V21 >= 0]). eq(gt(V, V1, Out),1,[],[Out = 1,V23 >= 0,V = 0,V1 = V23]). eq(gt(V, V1, Out),1,[],[Out = 2,V24 >= 0,V = 1 + V24,V1 = 0]). eq(gt(V, V1, Out),1,[gt(V25, V26, Ret7)],[Out = Ret7,V1 = 1 + V26,V25 >= 0,V26 >= 0,V = 1 + V25]). eq(ge(V, V1, Out),1,[],[Out = 2,V27 >= 0,V = V27,V1 = 0]). eq(ge(V, V1, Out),1,[],[Out = 1,V1 = 1 + V28,V28 >= 0,V = 0]). eq(ge(V, V1, Out),1,[ge(V29, V30, Ret8)],[Out = Ret8,V1 = 1 + V30,V29 >= 0,V30 >= 0,V = 1 + V29]). eq(minus(V, V1, Out),0,[],[Out = 0,V31 >= 0,V32 >= 0,V = V31,V1 = V32]). eq(gt(V, V1, Out),0,[],[Out = 0,V33 >= 0,V34 >= 0,V = V33,V1 = V34]). eq(ge(V, V1, Out),0,[],[Out = 0,V35 >= 0,V36 >= 0,V = V35,V1 = V36]). eq(if(V, V1, V4, Out),0,[],[Out = 0,V37 >= 0,V4 = V38,V39 >= 0,V = V37,V1 = V39,V38 >= 0]). eq(if1(V, V1, V4, Out),0,[],[Out = 0,V40 >= 0,V4 = V41,V42 >= 0,V = V40,V1 = V42,V41 >= 0]). eq(if2(V, V1, V4, Out),0,[],[Out = 0,V43 >= 0,V4 = V44,V45 >= 0,V = V43,V1 = V45,V44 >= 0]). eq(if3(V, V1, V4, Out),0,[],[Out = 0,V46 >= 0,V4 = V47,V48 >= 0,V = V46,V1 = V48,V47 >= 0]). input_output_vars(minus(V,V1,Out),[V,V1],[Out]). input_output_vars(if(V,V1,V4,Out),[V,V1,V4],[Out]). input_output_vars(gcd(V,V1,Out),[V,V1],[Out]). input_output_vars(if1(V,V1,V4,Out),[V,V1,V4],[Out]). input_output_vars(if2(V,V1,V4,Out),[V,V1,V4],[Out]). input_output_vars(if3(V,V1,V4,Out),[V,V1,V4],[Out]). input_output_vars(gt(V,V1,Out),[V,V1],[Out]). input_output_vars(ge(V,V1,Out),[V,V1],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [ge/3]
1. recursive : [gt/3]
2. recursive : [if/4,minus/3]
3. recursive : [gcd/3,if1/4,if2/4,if3/4]
4. non_recursive : [start/3]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into ge/3
1. SCC is partially evaluated into gt/3
2. SCC is partially evaluated into minus/3
3. SCC is partially evaluated into gcd/3
4. SCC is partially evaluated into start/3
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations ge/3
* CE 35 is refined into CE [36]
* CE 32 is refined into CE [37]
* CE 33 is refined into CE [38]
* CE 34 is refined into CE [39]
### Cost equations --> "Loop" of ge/3
* CEs [39] --> Loop 18
* CEs [36] --> Loop 19
* CEs [37] --> Loop 20
* CEs [38] --> Loop 21
### Ranking functions of CR ge(V,V1,Out)
* RF of phase [18]: [V,V1]
#### Partial ranking functions of CR ge(V,V1,Out)
* Partial RF of phase [18]:
- RF of loop [18:1]:
V
V1
### Specialization of cost equations gt/3
* CE 20 is refined into CE [40]
* CE 18 is refined into CE [41]
* CE 17 is refined into CE [42]
* CE 19 is refined into CE [43]
### Cost equations --> "Loop" of gt/3
* CEs [43] --> Loop 22
* CEs [40] --> Loop 23
* CEs [41] --> Loop 24
* CEs [42] --> Loop 25
### Ranking functions of CR gt(V,V1,Out)
* RF of phase [22]: [V,V1]
#### Partial ranking functions of CR gt(V,V1,Out)
* Partial RF of phase [22]:
- RF of loop [22:1]:
V
V1
### Specialization of cost equations minus/3
* CE 21 is refined into CE [44,45,46,47]
* CE 22 is refined into CE [48]
* CE 24 is refined into CE [49]
* CE 23 is refined into CE [50,51]
### Cost equations --> "Loop" of minus/3
* CEs [51] --> Loop 26
* CEs [50] --> Loop 27
* CEs [44,45,46,47,48,49] --> Loop 28
### Ranking functions of CR minus(V,V1,Out)
* RF of phase [26]: [V-1,V-V1]
* RF of phase [27]: [V]
#### Partial ranking functions of CR minus(V,V1,Out)
* Partial RF of phase [26]:
- RF of loop [26:1]:
V-1
V-V1
* Partial RF of phase [27]:
- RF of loop [27:1]:
V
### Specialization of cost equations gcd/3
* CE 26 is refined into CE [52]
* CE 29 is refined into CE [53]
* CE 25 is refined into CE [54,55,56,57]
* CE 28 is refined into CE [58,59,60,61]
* CE 31 is refined into CE [62,63,64,65,66]
* CE 30 is refined into CE [67,68]
* CE 27 is refined into CE [69,70]
### Cost equations --> "Loop" of gcd/3
* CEs [68] --> Loop 29
* CEs [70] --> Loop 30
* CEs [69] --> Loop 31
* CEs [67] --> Loop 32
* CEs [53] --> Loop 33
* CEs [58,59,63] --> Loop 34
* CEs [52] --> Loop 35
* CEs [54,55,56,57,60,61,62,64,65,66] --> Loop 36
### Ranking functions of CR gcd(V,V1,Out)
* RF of phase [29,30]: [V+V1-2]
#### Partial ranking functions of CR gcd(V,V1,Out)
* Partial RF of phase [29,30]:
- RF of loop [29:1]:
V-1
V-V1 depends on loops [30:1]
- RF of loop [30:1]:
-V+V1 depends on loops [29:1]
V1-1
### Specialization of cost equations start/3
* CE 7 is refined into CE [71,72,73,74,75,76,77,78]
* CE 8 is refined into CE [79,80,81]
* CE 9 is refined into CE [82]
* CE 10 is refined into CE [83,84,85,86,87,88]
* CE 11 is refined into CE [89,90,91,92,93,94,95,96,97]
* CE 12 is refined into CE [98,99,100]
* CE 2 is refined into CE [101,102,103]
* CE 3 is refined into CE [104]
* CE 4 is refined into CE [105]
* CE 5 is refined into CE [106]
* CE 6 is refined into CE [107,108,109,110,111,112]
* CE 13 is refined into CE [113,114,115]
* CE 14 is refined into CE [116,117,118,119,120,121]
* CE 15 is refined into CE [122,123,124,125,126]
* CE 16 is refined into CE [127,128,129,130,131]
### Cost equations --> "Loop" of start/3
* CEs [113,118,123,128] --> Loop 37
* CEs [79,82,89,90,93,98] --> Loop 38
* CEs [71,72,73,74,75,76,77,78,80,81,83,84,85,86,87,88,91,92,94,95,96,97,99,100] --> Loop 39
* CEs [101,102,103,105,106,107,108,109,110,111,112] --> Loop 40
* CEs [104,114,115,116,117,119,120,121,122,124,125,126,127,129,130,131] --> Loop 41
### Ranking functions of CR start(V,V1,V4)
#### Partial ranking functions of CR start(V,V1,V4)
Computing Bounds
=====================================
#### Cost of chains of ge(V,V1,Out):
* Chain [[18],21]: 1*it(18)+1
Such that:it(18) =< V
with precondition: [Out=1,V>=1,V1>=V+1]
* Chain [[18],20]: 1*it(18)+1
Such that:it(18) =< V1
with precondition: [Out=2,V1>=1,V>=V1]
* Chain [[18],19]: 1*it(18)+0
Such that:it(18) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [21]: 1
with precondition: [V=0,Out=1,V1>=1]
* Chain [20]: 1
with precondition: [V1=0,Out=2,V>=0]
* Chain [19]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of gt(V,V1,Out):
* Chain [[22],25]: 1*it(22)+1
Such that:it(22) =< V
with precondition: [Out=1,V>=1,V1>=V]
* Chain [[22],24]: 1*it(22)+1
Such that:it(22) =< V1
with precondition: [Out=2,V1>=1,V>=V1+1]
* Chain [[22],23]: 1*it(22)+0
Such that:it(22) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [25]: 1
with precondition: [V=0,Out=1,V1>=0]
* Chain [24]: 1
with precondition: [V1=0,Out=2,V>=1]
* Chain [23]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of minus(V,V1,Out):
* Chain [[27],28]: 3*it(27)+2*s(4)+3
Such that:aux(1) =< V-Out
it(27) =< Out
s(4) =< aux(1)
with precondition: [V1=0,Out>=1,V>=Out]
* Chain [[26],28]: 3*it(26)+2*s(3)+2*s(4)+1*s(9)+3
Such that:aux(1) =< V-Out
it(26) =< Out
aux(4) =< V1
s(4) =< aux(1)
s(3) =< aux(4)
s(9) =< it(26)*aux(4)
with precondition: [V1>=1,Out>=1,V>=Out+V1]
* Chain [28]: 2*s(3)+2*s(4)+3
Such that:aux(1) =< V
aux(2) =< V1
s(4) =< aux(1)
s(3) =< aux(2)
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of gcd(V,V1,Out):
* Chain [[29,30],36]: 8*it(29)+8*it(30)+7*s(11)+5*s(46)+3*s(47)+1*s(49)+3*s(52)+3*s(53)+2*s(54)+1*s(55)+4
Such that:aux(13) =< -V+V1
aux(10) =< V-V1
aux(21) =< V
aux(22) =< V+V1
aux(23) =< V1
s(11) =< aux(22)
it(29) =< aux(21)
it(29) =< aux(22)
it(30) =< aux(22)
s(57) =< aux(22)
it(30) =< aux(23)
s(57) =< aux(23)
it(30) =< aux(22)+aux(13)
it(29) =< aux(22)+aux(10)
s(53) =< it(30)*aux(23)
s(47) =< it(29)*aux(21)
s(52) =< s(57)
s(54) =< aux(23)
s(55) =< s(53)*aux(21)
s(46) =< aux(21)
s(49) =< s(47)*aux(23)
with precondition: [Out=0,V>=1,V1>=1,V+V1>=3]
* Chain [[29,30],32,36]: 8*it(29)+8*it(30)+9*s(14)+5*s(46)+3*s(47)+1*s(49)+3*s(52)+3*s(53)+2*s(54)+1*s(55)+12
Such that:aux(13) =< -V+V1
aux(10) =< V-V1
aux(26) =< V
aux(27) =< V+V1
aux(28) =< V1
s(14) =< aux(27)
it(29) =< aux(26)
it(29) =< aux(27)
it(30) =< aux(27)
s(57) =< aux(27)
it(30) =< aux(28)
s(57) =< aux(28)
it(30) =< aux(27)+aux(13)
it(29) =< aux(27)+aux(10)
s(53) =< it(30)*aux(28)
s(47) =< it(29)*aux(26)
s(52) =< s(57)
s(54) =< aux(28)
s(55) =< s(53)*aux(26)
s(46) =< aux(26)
s(49) =< s(47)*aux(28)
with precondition: [Out=0,V>=1,V1>=1,V+V1>=3]
* Chain [[29,30],32,35]: 8*it(29)+8*it(30)+7*s(46)+3*s(47)+1*s(49)+3*s(52)+3*s(53)+2*s(54)+1*s(55)+3*s(58)+13
Such that:aux(13) =< -V+V1
aux(10) =< V-V1
aux(16) =< V+V1
aux(17) =< V+V1-Out
aux(19) =< V1
aux(20) =< V1-Out
aux(24) =< Out
aux(29) =< V
s(58) =< aux(24)
s(46) =< aux(29)
it(29) =< aux(29)
aux(9) =< aux(16)
it(29) =< aux(16)
it(30) =< aux(16)
s(57) =< aux(16)
aux(9) =< aux(17)
it(29) =< aux(17)
it(30) =< aux(17)
s(57) =< aux(17)
it(30) =< aux(19)
s(56) =< aux(19)
s(57) =< aux(19)
it(30) =< aux(20)
s(56) =< aux(20)
s(57) =< aux(20)
it(30) =< aux(9)+aux(13)
it(29) =< aux(9)+aux(10)
s(53) =< it(30)*aux(19)
s(47) =< it(29)*aux(29)
s(52) =< s(57)
s(54) =< s(56)
s(55) =< s(53)*aux(29)
s(49) =< s(47)*aux(19)
with precondition: [Out>=1,V>=Out,V1>=Out,V+V1>=3*Out]
* Chain [[29,30],31,36]: 8*it(29)+8*it(30)+8*s(11)+5*s(46)+3*s(47)+1*s(49)+3*s(52)+3*s(53)+2*s(54)+1*s(55)+12
Such that:aux(13) =< -V+V1
aux(10) =< V-V1
aux(32) =< V
aux(33) =< V+V1
aux(34) =< V1
s(11) =< aux(33)
it(29) =< aux(32)
it(29) =< aux(33)
it(30) =< aux(33)
s(57) =< aux(33)
it(30) =< aux(34)
s(57) =< aux(34)
it(30) =< aux(33)+aux(13)
it(29) =< aux(33)+aux(10)
s(53) =< it(30)*aux(34)
s(47) =< it(29)*aux(32)
s(52) =< s(57)
s(54) =< aux(34)
s(55) =< s(53)*aux(32)
s(46) =< aux(32)
s(49) =< s(47)*aux(34)
with precondition: [Out=0,V>=1,V1>=2,V+2*V1>=7]
* Chain [[29,30],31,34]: 8*it(29)+8*it(30)+5*s(46)+3*s(47)+1*s(49)+3*s(52)+3*s(53)+2*s(54)+1*s(55)+5*s(63)+12
Such that:aux(13) =< -V+V1
aux(10) =< V-V1
aux(35) =< V
aux(36) =< V+V1
aux(37) =< V1
s(63) =< aux(36)
it(29) =< aux(35)
it(29) =< aux(36)
it(30) =< aux(36)
s(57) =< aux(36)
it(30) =< aux(37)
s(57) =< aux(37)
it(30) =< aux(36)+aux(13)
it(29) =< aux(36)+aux(10)
s(53) =< it(30)*aux(37)
s(47) =< it(29)*aux(35)
s(52) =< s(57)
s(54) =< aux(37)
s(55) =< s(53)*aux(35)
s(46) =< aux(35)
s(49) =< s(47)*aux(37)
with precondition: [Out=0,V>=1,V1>=2,V+2*V1>=7]
* Chain [[29,30],31,33]: 8*it(29)+8*it(30)+5*s(46)+3*s(47)+1*s(49)+3*s(52)+3*s(53)+4*s(54)+1*s(55)+3*s(63)+13
Such that:aux(13) =< -V+V1
aux(15) =< V
aux(10) =< V-V1
aux(16) =< V+V1
aux(17) =< V+V1-Out
aux(18) =< V-Out
aux(30) =< Out
aux(38) =< V1
s(63) =< aux(30)
s(54) =< aux(38)
it(29) =< aux(15)
s(50) =< aux(15)
aux(9) =< aux(16)
it(29) =< aux(16)
it(30) =< aux(16)
s(57) =< aux(16)
aux(9) =< aux(17)
it(29) =< aux(17)
it(30) =< aux(17)
s(57) =< aux(17)
it(29) =< aux(18)
s(50) =< aux(18)
it(30) =< aux(38)
s(57) =< aux(38)
it(30) =< aux(9)+aux(13)
it(29) =< aux(9)+aux(10)
s(53) =< it(30)*aux(38)
s(47) =< it(29)*aux(15)
s(52) =< s(57)
s(55) =< s(53)*aux(15)
s(46) =< s(50)
s(49) =< s(47)*aux(38)
with precondition: [Out>=1,V>=Out,V1>=Out+1,V+2*V1>=4*Out+3,V+V1>=3*Out+1]
* Chain [36]: 3*s(11)+4*s(14)+4
Such that:aux(5) =< V
aux(6) =< V1
s(11) =< aux(5)
s(14) =< aux(6)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [35]: 5
with precondition: [V=0,V1=Out,V1>=1]
* Chain [34]: 4
with precondition: [V1=0,Out=0,V>=0]
* Chain [33]: 5
with precondition: [V1=0,V=Out,V>=0]
* Chain [32,36]: 7*s(14)+2*s(61)+12
Such that:s(59) =< V
aux(25) =< V1
s(14) =< aux(25)
s(61) =< s(59)
with precondition: [Out=0,V1>=1,V>=V1]
* Chain [32,35]: 3*s(58)+2*s(61)+13
Such that:s(59) =< V
aux(24) =< Out
s(58) =< aux(24)
s(61) =< s(59)
with precondition: [V1=Out,V1>=1,V>=V1]
* Chain [31,36]: 6*s(11)+2*s(66)+12
Such that:s(64) =< V1
aux(31) =< V
s(11) =< aux(31)
s(66) =< s(64)
with precondition: [Out=0,V>=1,V1>=V+1]
* Chain [31,34]: 3*s(63)+2*s(66)+12
Such that:aux(30) =< V
s(64) =< V1
s(63) =< aux(30)
s(66) =< s(64)
with precondition: [Out=0,V>=1,V1>=V+1]
* Chain [31,33]: 3*s(63)+2*s(66)+13
Such that:s(64) =< V1
aux(30) =< Out
s(63) =< aux(30)
s(66) =< s(64)
with precondition: [V=Out,V>=1,V1>=V+1]
#### Cost of chains of start(V,V1,V4):
* Chain [41]: 66*s(193)+42*s(194)+1*s(200)+29*s(206)+48*s(207)+48*s(208)+18*s(210)+18*s(211)+18*s(212)+6*s(214)+6*s(216)+13
Such that:aux(55) =< -V+V1
aux(56) =< V
aux(57) =< V-V1
aux(58) =< V+V1
aux(59) =< V1
s(193) =< aux(56)
s(194) =< aux(59)
s(206) =< aux(58)
s(207) =< aux(56)
s(207) =< aux(58)
s(208) =< aux(58)
s(209) =< aux(58)
s(208) =< aux(59)
s(209) =< aux(59)
s(208) =< aux(58)+aux(55)
s(207) =< aux(58)+aux(57)
s(210) =< s(208)*aux(59)
s(211) =< s(207)*aux(56)
s(212) =< s(209)
s(214) =< s(210)*aux(56)
s(216) =< s(211)*aux(59)
s(200) =< s(193)*aux(59)
with precondition: [V>=0,V1>=0]
* Chain [40]: 56*s(267)+126*s(268)+32*s(275)+12*s(279)+4*s(294)+37*s(300)+48*s(301)+48*s(302)+18*s(304)+18*s(305)+18*s(306)+6*s(308)+6*s(310)+19
Such that:aux(70) =< -2*V1+V4
aux(71) =< V1
aux(72) =< V1+V4
aux(73) =< V4
s(267) =< aux(73)
s(300) =< aux(72)
s(301) =< aux(71)
s(301) =< aux(72)
s(302) =< aux(72)
s(303) =< aux(72)
s(302) =< aux(73)
s(303) =< aux(73)
s(302) =< aux(72)+aux(70)
s(301) =< aux(72)+aux(71)
s(304) =< s(302)*aux(73)
s(305) =< s(301)*aux(71)
s(306) =< s(303)
s(308) =< s(304)*aux(71)
s(268) =< aux(71)
s(310) =< s(305)*aux(73)
s(294) =< s(267)*aux(71)
s(275) =< aux(71)
s(275) =< aux(71)+aux(71)
s(279) =< s(275)*aux(71)
with precondition: [V=1,V1>=0,V4>=0]
* Chain [39]: 354*s(371)+96*s(383)+36*s(385)+295*s(395)+32*s(402)+12*s(406)+4*s(421)+95*s(427)+48*s(428)+48*s(429)+18*s(431)+18*s(432)+54*s(433)+6*s(435)+6*s(437)+9*s(527)+96*s(534)+96*s(535)+36*s(537)+36*s(538)+12*s(541)+12*s(543)+19
Such that:aux(108) =< -2*V1+V4
aux(109) =< V1
aux(110) =< V1-2*V4
aux(111) =< V1+V4
aux(112) =< V4
s(371) =< aux(112)
s(427) =< aux(111)
s(428) =< aux(109)
s(428) =< aux(111)
s(429) =< aux(111)
s(430) =< aux(111)
s(429) =< aux(112)
s(430) =< aux(112)
s(429) =< aux(111)+aux(108)
s(428) =< aux(111)+aux(109)
s(431) =< s(429)*aux(112)
s(432) =< s(428)*aux(109)
s(433) =< s(430)
s(435) =< s(431)*aux(109)
s(395) =< aux(109)
s(437) =< s(432)*aux(112)
s(421) =< s(371)*aux(109)
s(527) =< s(395)*aux(112)
s(383) =< aux(112)
s(383) =< aux(112)+aux(112)
s(385) =< s(383)*aux(112)
s(534) =< aux(109)
s(534) =< aux(111)
s(535) =< aux(111)
s(535) =< aux(112)
s(535) =< aux(111)+aux(112)
s(534) =< aux(111)+aux(110)
s(537) =< s(535)*aux(112)
s(538) =< s(534)*aux(109)
s(541) =< s(537)*aux(109)
s(543) =< s(538)*aux(112)
s(402) =< aux(109)
s(402) =< aux(109)+aux(109)
s(406) =< s(402)*aux(109)
with precondition: [V=2,V1>=0,V4>=0]
* Chain [38]: 80*s(719)+32*s(727)+12*s(731)+16
Such that:aux(117) =< V1
s(719) =< aux(117)
s(727) =< aux(117)
s(727) =< aux(117)+aux(117)
s(731) =< s(727)*aux(117)
with precondition: [V=2,V4=0,V1>=0]
* Chain [37]: 5*s(748)+5
Such that:aux(118) =< V
s(748) =< aux(118)
with precondition: [V1=0,V>=0]
Closed-form bounds of start(V,V1,V4):
-------------------------------------
* Chain [41] with precondition: [V>=0,V1>=0]
- Upper bound: 114*V+13+18*V*V+ (V+V1)* (6*V*V1)+42*V1+V1*V+6*V1*V*V+ (V+V1)* (18*V1)+ (95*V+95*V1)
- Complexity: n^3
* Chain [40] with precondition: [V=1,V1>=0,V4>=0]
- Upper bound: 206*V1+19+30*V1*V1+4*V1*V4+ (V1+V4)* (6*V1*V4)+56*V4+6*V4*V1*V1+ (V1+V4)* (18*V4)+ (103*V1+103*V4)
- Complexity: n^3
* Chain [39] with precondition: [V=2,V1>=0,V4>=0]
- Upper bound: 471*V1+19+66*V1*V1+4*V1*V4+ (V1+V4)* (18*V1*V4)+450*V4+9*V4*V1+18*V4*V1*V1+36*V4*V4+ (V1+V4)* (54*V4)+ (293*V1+293*V4)
- Complexity: n^3
* Chain [38] with precondition: [V=2,V4=0,V1>=0]
- Upper bound: 112*V1+16+12*V1*V1
- Complexity: n^2
* Chain [37] with precondition: [V1=0,V>=0]
- Upper bound: 5*V+5
- Complexity: n
### Maximum cost of start(V,V1,V4): max([5*V,42*V1+8+max([18*V*V+114*V+ (V+V1)* (6*V*V1)+V1*V+6*V1*V*V+ (V+V1)* (18*V1)+ (95*V+95*V1),36*V1*V1+265*V1+12*V1*nat(V4)*nat(V1+V4)+nat(V4)*394+nat(V4)*9*V1+nat(V4)*12*V1*V1+nat(V4)*36*nat(V4)+nat(V4)*36*nat(V1+V4)+nat(V1+V4)*190+ (94*V1+3+18*V1*V1+4*V1*nat(V4)+6*V1*nat(V4)*nat(V1+V4)+nat(V4)*56+nat(V4)*6*V1*V1+nat(V4)*18*nat(V1+V4)+nat(V1+V4)*103)+ (70*V1+3+12*V1*V1)])])+5
Asymptotic class: n^3
* Total analysis performed in 1400 ms.